data($T$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$x$:Id$\times$$T$($x$)